T:Type, n:, h, f:(T(T + Top)). f^n o h   = primrec(n;h;i,g. f o g  )  T(T + Top) 

latex

ProofTree

Definitions	Void, a < b, n - m, n+m, -n, #$n, A  B, A, False, i  j , P  Q, {x:A| B(x)} , Type, x:A. B(x), s = t, left + right, Top, x:AB(x), t  T, , f^n, , s ~ t, , SQType(T), {T}, P  Q, P & Q, x:A  B(x), P  Q, primrec(n;b;c), p-id(), x.A(x), f o g  , {i..j}, T, True
Lemmas	top wf, true wf, squash wf, p-compose-associative, le wf, int seg wf, p-compose wf, p-id wf, primrec wf, primrec add, p-id-compose, nat wf, nat properties, ge wf